$\forall$${\it the\_es}$:ES, $l$:IdLnk, ${\it e'}$:E, $m$:(Msg on $l$).
\\[0ex]($m$ $\in$ msgs($l$;before(${\it e'}$))) $\Leftarrow\!\Rightarrow$ ($\exists$$e$:E. ((($e$ $<$loc ${\it e'}$) \& ($\uparrow$haslnk($l$;$e$))) c$\wedge$ ($m$ = emsg($e$))))